Added the ability to reflect Inductive definitions #32

aa755 · 2016-12-01T23:54:53Z

This is implemented as the command Make Inductive.
See demo.v for a demo.

Just created a new vernac command "Make Inductive". As of now, it does nothing. Tested the dummy command in demo.v

The body is ignored for now. Tested this part in demo.v

The name and arity are obtained properly populated. However the resultant definition changes arity from Set to Prop.

Found the correct input by snooping on the paramcoq plugin (using coq/dev/top_printer.ml) Also, needed to recompile coq so that top_printer.ml gets included in coqtop/coqc: coq/dev$ echo "Top_printer" > printer.mllib then add dev/printer.cma to $CORECMA in coq/Makefile.common

…to coq-8.5

gmalecha · 2016-12-02T03:25:39Z

Thanks for the PR. This is a great feature to have.

Is there a reason that you chose not to use the existing quoting of inductive types? In particular (https://github.com/gmalecha/template-coq/blob/master/theories/Ast.v#L63) Does it not contain enough information? My worry with exposing such low level types is two fold:

They don't fit naturally into the mental model that users have (maybe that is the wrong mental model?)
They are difficult (verbose?) to program with.

aa755 · 2016-12-02T03:41:10Z

That information is not sufficient, as pointed out by Jason:
#17

All the fields in Ast.mutual_inductive_entry and Ast.one_inductive_entry (except maybe mind_entry_private) seem semantically relevant to me.

gmalecha · 2016-12-02T03:50:08Z

I don't doubt that they are semantically relevant, it just seems like it is a representation that is not natural to Coq users.

To address the problem that @JasonGross pointed out, would it be sufficient to add a type to the inductive as a whole? Something like:

| PType : ident -> term (* the type *)-> list (ident * inductive_body) -> program -> program

My worry is that everyone that uses this library is going to have to reverse engineer what this type does. A better solution (if it can be made to work) would be to have something that maps more directly to how Coq users write inductive types.

aa755 · 2016-12-02T04:24:04Z

I did have some difficulty in figuring out the de-bruijn indices for the types of constructors.
I may sometime write in Gallina a high-level wrapper to compute the argument to Make Inductive, perhaps from something that is named (instead of de-bruijn) and looks close to how Coq users write inductives. However, I would prefer to keep the OCaml part (in reify.ml4) as simple as possible.

Your suggested representation still loses information that is relevant to me (parameters vs indices, flags for template/universe polymorphism).

JasonGross · 2016-12-02T05:32:00Z

I believe mind_entry_private is about whether or not it's okay to pattern match on the inductive outside the module it's defined in; this is to allow Licata's HIT trick.

mattam82

I agree with @gmalecha that it would be nicer to find a way to merge this info in PType somehow, otherwise we have a strange redundancy. Currently template-coq has this "program" datatypes that does not correspond to something in Coq. Why not switch to an env + term representation here?
Then the inductive decls and global definitions would be in the env. We could make a compatibility layer that would produce a [program] from those.

mattam82 · 2016-12-02T10:56:15Z

theories/Ast.v

+
+
+Definition local_entry : Set := term.
+(*


Why not LocalDef and LocalAssum here?

Does LocalDef stand for local let bindings?

mattam82 · 2016-12-02T10:56:45Z

theories/Ast.v

+
+Record mutual_inductive_entry : Set := {
+  mind_entry_record : option (option ident); 
+(*  mind_entry_finite : Decl_kinds.recursivity_kind;  (* inductive/coinductive/record*)*)


I think the finiteness information can be useful (ind vs coind in particular)

I agree. I was being lazy.

mattam82 · 2016-12-02T10:58:11Z

theories/Ast.v

+  mind_entry_params : list (ident * local_entry);
+  mind_entry_inds : list one_inductive_entry;
+  mind_entry_polymorphic : bool; 
+(*  mind_entry_universes : Univ.universe_context; (*what is this?*) *)


It's the universe context of the inductive: either global universes and constraints that must be declared or local in case of universe polymorphism (it records the universe binders of all the inductives/constructors in that case). This is not handled by template-coq anywhere currently.

I had a lot of issues trying to get this to work due to the way that Coq represents universes. Issue #1 is about universes. If you have any thoughts on how to reify and reflect universes, I think that is the biggest problem with template-coq right now.

mattam82 · 2016-12-02T10:58:31Z

theories/Ast.v

+  mind_entry_inds : list one_inductive_entry;
+  mind_entry_polymorphic : bool; 
+(*  mind_entry_universes : Univ.universe_context; (*what is this?*) *)
+  mind_entry_private : option bool


Indeed private is for the HIT trick

gmalecha · 2016-12-02T13:17:05Z

I think then env + term representation would be a good route to go here. At minimum this would mean pulling the constructors of program out and make them the environment values.

@mattam82 I got confused about the last comment in your comment. Do you think that we should convert these new definitions to something like PType in Gallina, or in the plugin?

mattam82 · 2016-12-02T14:33:27Z

@gmalecha in Gallina, as part of the plugin's v files we could have an env + term -> program function to get back the closed representation.

mattam82 · 2016-12-02T16:40:52Z

Yes

…

On Fri, Dec 2, 2016 at 5:14 PM Abhishek Anand ***@***.***> wrote: ***@***.**** commented on this pull request. ------------------------------ In theories/Ast.v <#32>: > @@ -63,3 +63,34 @@ Inductive program : Set := list (ident * inductive_body) -> program -> program | PAxiom : ident -> term (* the type *) -> program -> program | PIn : term -> program. + + +(* representation of mutual inductives. copied, more or less, from Coq/kernel/entries.mli +*) + +Record one_inductive_entry : Set := { + mind_entry_typename : ident; + mind_entry_arity : term; + mind_entry_template : bool; (* template polymorphism ? *) + mind_entry_consnames : list ident; + mind_entry_lc : list term}. + + +Definition local_entry : Set := term. +(* Does LocalDef stand for local let bindings? — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#32>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAGARSu5ImchGCkEzBJIq0dfim9Ls2OCks5rEEPkgaJpZM4LCCXt> .

gmalecha · 2016-12-04T04:06:55Z

@aa755 Why don't we export the entire type for this PR, and then open a second issue and PR to add the environment representation that @mattam82 suggested. That will let us merge this relatively quickly and it won't break anything for users.

gmalecha · 2016-12-06T03:23:51Z

test-suite/demo.v

+  mind_entry_private := None;
+|}.
+
+(* Make Inductive ltac:(let t:= eval compute in mut_i in exact t). *)


Can we make this perform reduction so that we don't need to use tactics in terms to make it work? I don't know precisely how to do this, but I'm certain that @mattam82 could tell us in a minute.

gmalecha · 2016-12-06T03:25:54Z

theories/Ast.v

+  | Finite
+  | CoFinite
+  | BiFinite
+*)


This seems like an out-of-place comment.

gmalecha · 2016-12-06T03:26:43Z

theories/Ast.v

+  | LocalDef of constr
+  | LocalAssum of constr
+*)
+


(** The kind of definition. See kerne/....mli **)

gmalecha · 2016-12-06T03:27:11Z

theories/Ast.v

+type local_entry =
+  | LocalDef of constr
+  | LocalAssum of constr
+*)


Like the next comment.

gmalecha · 2016-12-06T03:28:34Z

src/reify.ml4

+VERNAC COMMAND EXTEND Unquote_inductive CLASSIFIED AS SIDEFF
+    | [ "Make" "Inductive" constr(def) ] ->
+      [ check_inside_section () ;
+	let (evm,env) = Lemmas.get_current_context () in


Is it necessary to check_inside_section here?

gmalecha · 2016-12-06T03:28:56Z

src/reify.ml4

@@ -766,6 +826,14 @@ VERNAC COMMAND EXTEND Unquote_vernac CLASSIFIED AS SIDEFF
 	  [] None result None (Lemmas.mk_hook (fun _ _ -> ())) ]
 END;;

+(* get rid of the unused ident(name)? *)


What does this mean?

gmalecha · 2016-12-08T03:33:17Z

Merging!

Rename Constraint to ConstraintSet

aa755 added 15 commits November 14, 2016 23:33

started work on reflecting inductive definitions.

7c2969d

Just created a new vernac command "Make Inductive". As of now, it does nothing. Tested the dummy command in demo.v

The command can now declare an empty inductive of a give name.

4fac2ee

The body is ignored for now. Tested this part in demo.v

documented a bug in unquoting. It incorrectly changes Prop to Set.

4a71321

preliminary work on transparentification.

6a07c23

Defined kernel's representation of inductive datatypes.

3e025d6

started populating the inductive entries properly.

1d75c3f

The name and arity are obtained properly populated. However the resultant definition changes arity from Set to Prop.

bugfix : Prop and Set were switched

70bfe07

unable to construct the type of constructors. error.

11e9c1c

unquoted params, tested mutual and parametrized inductives.

7db60c9

Merge branch 'coq-8.5' of https://github.com/gmalecha/template-coq in…

c66334d

…to coq-8.5

cleaned up the demo

24cdc10

more cleanup for PR

6506e45

clearnup for PR

03905b7

removed the unused argument (name) in Make Inductive

834cbb1

gmalecha added the enhancement label Dec 2, 2016

mattam82 requested changes Dec 2, 2016

View reviewed changes

aa755 added 2 commits December 5, 2016 22:07

exported all members of mutual entry, except universe contexts

bdc1171

properly unquoted mind_entry_record

2fa5fdc

gmalecha reviewed Dec 6, 2016

View reviewed changes

properly unquoted mind_entry_finite

10f3993

aa755 added 2 commits December 5, 2016 22:38

properly unquoted mind_private

596619d

Make Inductive does reduction

fac3650

gmalecha merged commit db3da94 into gmalecha:coq-8.5 Dec 8, 2016

aa755 mentioned this pull request Dec 8, 2016

It would be nice if inductives stored their types #17

Open

gmalecha pushed a commit that referenced this pull request Jun 23, 2018

Merge pull request #32 from Template-Coq/renameConstraint

889b3d1

Rename Constraint to ConstraintSet

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Added the ability to reflect Inductive definitions #32

Added the ability to reflect Inductive definitions #32

aa755 commented Dec 1, 2016

gmalecha commented Dec 2, 2016

aa755 commented Dec 2, 2016 •

edited

Loading

gmalecha commented Dec 2, 2016

aa755 commented Dec 2, 2016

JasonGross commented Dec 2, 2016

mattam82 left a comment

mattam82 Dec 2, 2016

aa755 Dec 2, 2016

mattam82 Dec 2, 2016

aa755 Dec 2, 2016

mattam82 Dec 2, 2016

gmalecha Dec 2, 2016

mattam82 Dec 2, 2016

gmalecha commented Dec 2, 2016

mattam82 commented Dec 2, 2016 •

edited

Loading

mattam82 commented Dec 2, 2016 via email

gmalecha commented Dec 4, 2016

gmalecha Dec 6, 2016

gmalecha Dec 6, 2016

gmalecha Dec 6, 2016

gmalecha Dec 6, 2016

gmalecha Dec 6, 2016

gmalecha Dec 6, 2016

gmalecha commented Dec 8, 2016

Added the ability to reflect Inductive definitions #32

Added the ability to reflect Inductive definitions #32

Conversation

aa755 commented Dec 1, 2016

gmalecha commented Dec 2, 2016

aa755 commented Dec 2, 2016 • edited Loading

gmalecha commented Dec 2, 2016

aa755 commented Dec 2, 2016

JasonGross commented Dec 2, 2016

mattam82 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gmalecha commented Dec 2, 2016

mattam82 commented Dec 2, 2016 • edited Loading

mattam82 commented Dec 2, 2016 via email

gmalecha commented Dec 4, 2016

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gmalecha commented Dec 8, 2016

aa755 commented Dec 2, 2016 •

edited

Loading

mattam82 commented Dec 2, 2016 •

edited

Loading